Nuprl Lemma : fpf-single_wf2
0,22
postcript
pdf
A
,
B
:Type,
x
:
A
,
v
:
B
,
eqa
:EqDecider(
A
).
x
:
v
a
:
A
fp
x
:
B
(
a
)?Top
latex
Definitions
x
dom(
f
)
,
f
(
x
)
,
if
b
t
else
f
fi
,
p
q
,
eqof(
d
)
,
false
,
Top
,
x
:
v
,
x
.
t
(
x
)
,
f
(
x
)?
z
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
fpf-single
wf
,
top
wf
,
bfalse
wf
,
eqof
wf
,
bor
wf
,
ifthenelse
wf
,
eqof
eq
btrue
origin
A, B:Type, x:A, v:B, eqa:EqDecider(A). x : v 
a:A fp
x : B(a)?Top A, B:Type, x:A, v:B, eqa:EqDecider(A). x : v a:A fp x : B(a)?Top dom(f)
t else f fi
q
x. t(x)x:A. B(x) T